Nuprl Lemma : segment_wf
2,24
postcript
pdf
T
:Type,
as
:
T
List,
m
,
n
:
. (
as
[
m
..
n
])
T
List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
nth_tl(
n
;
as
)
,
firstn(
n
;
as
)
,
as
[
m
..
n
]
Lemmas
firstn
wf
,
nth
tl
wf
origin
T:Type, as:T List, m, n:
. (as[m..n
]) 
T List T:Type, as:T List, m, n:. (as[m..n]) T List Tx:A. B(x)]